| Definitions |  x:A. B(x), P   Q,  , t  T, A B,  A, False, i j, R-da(R;i), SQType(T), {T}, Prop, Top, if b t else f fi,   x. t(x), true, false, Valtype(da;k), Knd, f(x)?z, , x dom(f), deq-member(eq;x;L), 1of(t), reduce(f;k;as), Y, Realizer,  b, P & Q, R-interface-compat(A;B), Rplus?(x1), Rnone?(x1), Id,  , es realizer ind, True, A & B, P  Q, P Q, Rsends?(x1), left  right, @loc x initially v:T, @loc only events in L change x:T, only events in L send on lnk with tag, @loc: k writes only members of L, @loc: k sends only on links in L, @loc: only members of L read x, @loc effect knd(v:T) x := f State(ds) v , @loc precondition for a(v:T):P State(ds) v, sends knd(v:T) on l:tagged(g,State(ds),v):dt, Reffect?(x1), KindDeq, x : v, locl(a), rcv(l,tg), eqof(d), union-deq(A;B;a;b), sumdeq(a;b), p  q,  , A || B, P Q, x(s),  , Unit, R-Feasible(R), R-loc(R), let x = a in b(x), Reffect-knd(x1), Rsends-l(x1), Rsends-dt(x1), Reffect-T(x1), Rsends-knd(x1), Rsends-T(x1), isrcv(k), lnk(k), tag(k), p  q, isl(x), 2of(t), outl(x), , a = b |
| Lemmas | nat wf, R-size wf, nat plus wf, le wf, assert wf, isrcv wf, Knd wf, R-compat wf, R-Feasible wf, es realizer wf, nat properties, ge wf, bool cases, Rplus? wf, bool sq, bool wf, eqtt to assert, Rplus-implies, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, R-Feasible-Rplus, R-size-decreases, fpf-join-cap-sq, Kind-deq wf, R-da wf, Rplus-left wf, lsrc wf, lnk wf, fpf-trivial-subtype-top, fpf wf, top wf, Rplus-right wf, fpf-dom wf, ldst wf, Rnone? wf, Rnone-implies, ma-valtype wf, fpf-cap wf, IdLnk wf, Id wf, subtype rel self, deq wf, eq id wf, R-loc wf, assert-eq-id, not functionality wrt iff, R-da-Rda, subtype-fpf-cap5, Rda wf, unit wf, decl-state wf, decl-type wf, Rnone wf, true wf, false wf, R-interface-compat wf, Rplus wf, Rinit wf, Rframe wf, Rsframe wf, Raframe wf, Rbframe wf, Rrframe wf, Reffect wf, fpf-single wf, fpf-cap-single, eq knd wf, assert-eq-knd, Knd sq, fpf-join wf, lnk-decl wf, Rsends wf, locl wf, Rpre wf, ifthenelse wf, fpf-empty wf, fpf-single-dom, fpf-cap-single1, isrcv-implies, lnk-decl-cap2, tagof wf, eq lnk wf, assert-eq-lnk, id-deq wf, IdLnk sq, Id sq |
Valtype(R-da(B;destination(lnk(k)));k))